package simplytypeddebruijn

object TextualToAbstractTest extends Application {
  val p =   new SimplyTypedTextualToAbstractTransform  with AbstractSyntax with TextualSyntax
  import p._
  println  {textualtoabstract(RApp(RLam(RVarName("x"),RTyBool,RVarName("x")),RIf(RTru,RFls,RTru))) }
  println  {textualtoabstract(RLet(RVarName("x"),RTru,RLam(RVarName("x"),RTyBool,RVarName("x")))) }
  println  {textualtoabstract(RLet(RVarName("x"),RTru,RLam(RVarName("y"),RTyBool,RVarName("x")))) }
  //(\\f: (int => int) . \\x: bool. \\y: int. (f y)) (\\x: int . x) (true) (5)
  println  {textualtoabstract(RApp(RApp(RApp(
                                RLam(RVarName("f"),RTyArr(RTyInt,RTyInt),
                                    RLam(RVarName("x"),RTyBool,
                                        RLam(RVarName("y"),RTyInt, RApp(RVarName("f"),RVarName("y"))))),
                                RLam(RVarName("x"),RTyInt,RVarName("x"))),
                                    RTru),
                                    	RLit(5)) ) }

  
}

trait SimplyTypedTextualToAbstractTransform { self : SimplyTypedTextualToAbstractTransform with AbstractSyntax with TextualSyntax =>
  //used to convert to form with debruijn indices
  
  //type RawTerm   //merged from ConcreteSyntax
  //type RawType
  
  type CleanTerm = LTerm
  type CleanType = LType
  
  def textualtoabstract(t: RawTerm):CleanTerm= SimplyTypedDeBruijnify.fresh( t)

  object SimplyTypedDeBruijnify {
    def fresh= new DeBruijnifyCtxFun {val ctx = new StringBindingContext[NameBinding](Nil)
  }
  
  
  trait DeBruijnifyCtxFun extends ContextualFun[RawTerm,CleanTerm,DeBruijnifyCtxFun]{
    def create(ctxnew: Ctx)=  new DeBruijnifyCtxFun {val ctx = ctxnew}

    val hintTransform = {s:String => s}
    def onvar(str:String) =ctx.getIndexOfName(str)
    
    def apply(t:RawTerm):CleanTerm = toDeBruijn(t) 

    def toDeBruijn(t: RawTerm):CleanTerm =  t match {  
        case ty: RType            => toDeBruijnType(ty)
        case RTru()               => Tru()
        case RFls()               => Fls()
        case RLit(n)              => Lit(n)
        case RUnit()              => Unit()
        
        case RIf(cond,pos,neg)   => If(this(cond),this(pos),this(neg))
        case RLam(RVarName(str), ty,t) =>  Lam(str,toDeBruijnType(ty),extend(str)(t))
        case RVarName(str) =>  Var(onvar(str))
        case RLet(RVarName(str),conc:RawTerm,body:RawTerm) =>
           Let(str,toDeBruijn(conc),extend(str).toDeBruijn(body))
        case RApp(t1,t2)                => App(this (t1), this (t2))
            
        case RRecProj(t1:RawTerm,label)                 => RecProj(this (t1),label)
        case r@RRecord(fields:List[(String,RawTerm)])   => Record(r.map(this))
        
     }
    val toDeBruijnType = new Function1[RawType,CleanType]{
      def apply(r:RawType) = r match {
        case RTyBool() => TyBool
        case RTyInt()  => TyInt
        case RTyUnit() => TyUnit
        case r@RTyArr(ty1:RawType,ty2:RawType)           => TyArr(this(ty1),this(ty2)) 
        case r@RTyRecord(fields:List[(String, RawType)]) => TyRecord(r.map(this))
        }

    }
    
    

  } 
  }


}








